\subsection{Definitions}
\begin{definition}
    Let \( X \subseteq \mathcal M^n \) be a subset of an \( \mathcal L \)-structure \( \mathcal M \), and let \( P \subseteq \mathcal M \).
    We say that \( X \) is \emph{definable} in \( \mathcal L \) with \emph{parameters} in \( P \) if there is a tuple \( \vb p \in P \) and an \( \mathcal L_P \)-formula \( \varphi(\vb x, \vb y) \) such that
    \[ X = \varphi(\vb x, \vb p) = \qty{\vb m \in \mathcal M^n \mid \mathcal M \vDash \varphi(\vb m, \vb p)} \]
    If \( P = M \), we say that \( X \) is \emph{definable}.
\end{definition}
\begin{example}
    Consider the usual natural numbers as a structure for the language generated by the signature \( (+, \cdot, 0, 1) \).
    Then there is an \( \mathcal L \)-formula \( T(e, x, s) \) such that \( \mathbb N \vDash T(e, x, s) \) if and only if the Turing machine encoded by the number \( e \) halts on input \( x \) in at most \( s \) steps.
    Thus, the set of halting computations is definable in this language.
    In particular, this implies that the theory of \( \mathbb N \) is not decidable.
\end{example}
\begin{definition}
    Let \( \mathcal T \) be a theory and \( n \in \mathbb N \).
    We obtain an equivalence relation \( \sim \) on the set \( \mathcal L(\vb x) \) of \( \mathcal L \)-formulae with free variables \( \vb x \), where \( \vb x \) is a tuple of length \( n \), by setting
    \[ \varphi(\vb x) \sim \psi(\vb x) \iff \mathcal T \vdash \forall \vb x.\, (\varphi(\vb x) \Leftrightarrow \psi(\vb x)) \]
    The quotient \( \mathcal B_n(\mathcal T) = \faktor{\mathcal L(\vb x)}{\sim} \) becomes a Boolean algebra by setting \( [\varphi] \bowtie [\psi] = [\varphi \bowtie \psi] \) for any logical connective \( \bowtie \), called the \emph{Lindenbaum--Tarski algebra} of \( \mathcal T \) on variables \( \vb x \).
\end{definition}
\begin{definition}
    Let \( \mathcal M \) be an \( \mathcal L \)-structure and \( A \subseteq \mathcal M \).
    Let \( \mathcal T \) be the \( \mathcal L_A \)-theory of sentences with parameters in \( A \) that hold in \( \mathcal M \), denoted \( \operatorname{Th}_A(\mathcal M) \).
    The proper filters on the Boolean algebra \( \mathcal B_n(\mathcal T) \) are called the \emph{\( n \)-types} of \( \mathcal M \) over \( A \).
\end{definition}
\begin{remark}
    If \( \mathcal F \) is a proper filter on \( \mathcal B_n(\mathcal T) \), it cannot include the bottom element \( [\bot] \).
    This motivates the following more convenient definition of an \( n \)-type.
\end{remark}
\begin{definition}
    Let \( \mathcal M \) be an \( \mathcal L \)-structure and \( A \subseteq \mathcal M \).
    A set \( p \) of \( \mathcal L_A \)-formulae with \( n \) free variables \( \vb x \) is an \emph{\( n \)-type} of \( \mathcal M \) over \( A \) if \( p \cup \operatorname{Th}_A(\mathcal M) \) is satisfiable.
    More generally, if \( \mathcal T \) is a theory, we say that a set \( p \) of \( \mathcal L \)-formulae with \( n \) free variables \( \vb x \) is an \emph{\( n \)-type} of \( \mathcal T \) if
    \[ \mathcal T \cup \qty{\exists \vb x.\, \bigwedge \Psi} \]
    is consistent for all finite subsets \( \Psi \) of \( p \).
    An \( n \)-type \( p \) is called \emph{complete} if it is maximal among the collection of \( n \)-types, in the sense that for any \( \mathcal L \)-formula \( \varphi(\vb x) \), either \( \varphi \in p \) or \( \varphi \notin p \).
    We denote the set of complete \( n \)-types by \( S_n(\mathcal T) \), or \( S_n^{\mathcal M}(A) \) if \( \mathcal T = \operatorname{Th}_A(\mathcal M) \).
    An element \( \vb m \in \mathcal M^n \) \emph{realises} an \( n \)-type \( p \) in \( \mathcal M \) if \( \mathcal M \vDash \varphi(\vb m) \) holds for all \( \varphi \) in \( p \).
    If no element realises a type, we say that the type is \emph{omitted} in \( \mathcal M \).
\end{definition}
\begin{example}
    \begin{enumerate}
        \item Let \( \mathcal M = (\mathbb Q, <) \), and consider the formulae \( n < x \) for each natural number \( n \).
        This collection of formulae is a 1-type, as any finite subset is consistent with \( \operatorname{Th}_{\mathbb N}(\mathbb Q) \).
        This type is omitted in \( \mathbb Q \) as no rational number \( x \) satisfies all of the formulae \( n < x \) for \( n \in \mathbb N \).
        However, this type is realised in an elementary extension of \( \mathbb Q \).
        The realisers can be thought of as imaginary, infinitely large rationals.
        \item Consider \( \mathbb R \) as a structure for the theory of ordered fields.
        The set of formulae
        \[ \qty{0 < x < \frac{1}{n} \midd 0 < n \in \mathbb N} \]
        form a 1-type of infinitesimal real numbers.
        This type is omitted in \( \mathbb R \), but there is an elementary extension realising this type, such as the ultrapower with respect to a free ultrafilter.
        \item For any \( \mathcal L \)-structure \( \mathcal M \), subset \( A \subseteq \mathcal M \), and tuple \( \vb m \in \mathcal M \), we can form the \( n \)-type of all of the \( \mathcal L_A \)-formulae that hold in \( \mathcal M \) of \( \vb m \).
        \[ \operatorname{tp}^{\mathcal M}(\vb m/A) = \qty{\varphi(\vb x) \in \mathcal L_A \mid \mathcal M \vDash \varphi(\vb m)} \]
        This is a complete \( n \)-type, called \emph{the type of \( \vb m \)} over \( A \).
        This is a type corresponding to the principal filter on an equivalence class corresponding to an equality formula.
    \end{enumerate}
\end{example}
\begin{proposition}
    Let \( \mathcal M \) be an \( \mathcal L \)-structure with \( A \subseteq \mathcal M \) and let \( p \) be an \( n \)-type of \( \mathcal M \) over \( A \).
    Then there is an elementary extension \( \mathcal N \) of \( \mathcal M \) that realises \( p \).
\end{proposition}
\begin{proof}
    We use the method of diagrams, and show that
    \[ \Gamma = p \cup \operatorname{Diag}_{\text{el}}(\mathcal M) \]
    is satisfiable by compactness.
    Let \( \Delta \) be a finite subset of \( \Gamma \), and let
    \[ \varphi = \bigwedge_{\varphi' \in \Delta \cap p} \varphi';\quad \psi = \bigwedge_{\psi' \in \Delta \cap \operatorname{Diag}_{\text{el}}(\mathcal M)} \psi' \]
    Note that \( \Delta \) is satisfiable if and only if
    \[ \varphi(\vb x, \vb a) \wedge \psi(\vb a', \vb b) \]
    is satisfiable, where \( \vb a, \vb a' \in A \) and \( \vb b \in \mathcal M \setminus \mathcal A \), and
    \[ \varphi \in p;\quad \mathcal M \vDash \psi(\vb a', \vb b) \]
    As \( p \) is an \( n \)-type, there is an \( \mathcal L_A \)-structure \( \mathcal N_0 \) that satisfies \( p \cup \operatorname{Th}_A(\mathcal M) \).
    As \( \mathcal M \vDash \psi(\vb a', \vb b) \), we have \( \mathcal M \vDash \exists \vb y.\, \psi(\vb a', \vb y) \).
    Note that this is an \( \mathcal L_A \)-formula, so
    \[ (\exists \vb y.\, \psi(\vb a', \vb y)) \in \operatorname{Th}_A(\mathcal M) \]
    Hence,
    \[ \mathcal N_0 \vDash \varphi(\vb c, \vb a) \exists y.\, \psi(\vb a', \vb y) \]
    for some \( \vb c \in \mathcal N_0 \).
    Note that \( \mathcal N_0 \) is an \( \mathcal L_A \)-structure, not an \( \mathcal L_{\mathcal M} \)-structure.
    However, by interpreting \( \vb b \) in \( \mathcal N_0 \) as the witness \( \vb y \) to \( \exists \vb y.\, \psi(\vb a', \vb y) \), we make \( \mathcal N_0 \) into an \( \mathcal L_{\mathcal M} \)-structure; elements of \( \mathcal M \) not in \( A \) or \( \vb b \) are interpreted arbitrarily.
    In this \( \mathcal L_{\mathcal M} \)-structure, \( \Delta \) is satisfiable.
    Thus \( \Gamma \) is satisfiable by compactness.

    Now, let \( \mathcal N \) be an \( \mathcal L_{\mathcal M} \)-structure satisfying \( \Gamma \), so \( \mathcal N \) is an elementary extension of \( \mathcal M \).
    As \( \mathcal N \) satisfies \( p \), there must be a tuple \( \vb n \in \mathcal N \) with \( \mathcal N \vDash \varphi(\vb n) \) for each \( \varphi \in p \).
    In other words, \( \vb n \) realises \( p \) in \( \mathcal N \).
\end{proof}
\begin{corollary}
    An \( n \)-type \( p \) of \( \mathcal M \) over \( A \subseteq \mathcal M \) is complete if and only if there is an elementary extension \( \mathcal N \) of \( \mathcal M \) and some \( \vb a \in \mathcal N \) such that \( p = \operatorname{tp}^{\mathcal N}(\vb a/A) \).
\end{corollary}
\begin{proof}
    If \( \mathcal N \) is an elementary extension of \( \mathcal M \) and \( \vb a \in \mathcal N \), then
    \[ \operatorname{tp}^{\mathcal N}(\vb a/A) \in S_n^{\mathcal N}(A) = S_n^{\mathcal M}(A) \]
    as the extension is elementary.

    Conversely, if \( p \) is a complete \( n \)-type, then by the previous result, there is an elementary extension \( \mathcal N \) of \( \mathcal M \) with a tuple \( \vb a \) realising the type.
    As \( p \) is complete, every \( \mathcal L_A \)-formula \( \varphi \), either \( \varphi \in p \) or \( \varphi \notin p \), but not both.
    If \( \varphi \in \operatorname{tp}^{\mathcal N}(\vb a/A) \), then \( \mathcal N \vDash \varphi(\vb a) \), so we cannot have \( \varphi \notin p \), thus \( \varphi \in p \).
    Conversely, if \( \varphi \in p \), then \( \mathcal N \vDash \varphi(\vb a) \) as \( \vb a \) realises \( p \), so \( \varphi \in \operatorname{tp}^{\mathcal N}(\vb a/A) \).
    Thus \( p = \operatorname{tp}^{\mathcal N}(\vb a/A) \) as required.
\end{proof}

\subsection{Stone spaces}
Let \( \mathcal M \) be an \( \mathcal L \)-structure and let \( A \subseteq \mathcal M \).
For each formula \( \varphi \) on \( n \) variables, we consider the set of all complete types that include this formula, denoted
\[ \lBrack\varphi\rBrack = \qty{p \in S_n^{\mathcal M}(A) \mid \varphi \in p} \]
Note that
\[ \lBrack\varphi \vee \psi\rBrack = \lBrack\varphi\rBrack \cup \lBrack\psi\rBrack;\quad \lBrack\varphi \wedge \psi\rBrack = \lBrack\varphi\rBrack \cap \lBrack\psi\rBrack \]
These serve as the basic open sets for a topology on \( S_n^{\mathcal m}(A) \), so an open set is an arbitrary union of open sets of this form.
Moreover, each of these basic open sets \( \lBrack\varphi\rBrack \) is the complement of another basic open set \( \lBrack\neg\varphi\rBrack \), so these open sets are also closed.
The \( S_n^{\mathcal M}(A) \) are called \emph{Stone spaces}, which are compact and totally disconnected topological spaces.
\begin{example}
    Let \( F \) be an algebraically closed field, and let \( k \) be a subfield of \( F \).
    The complete \( n \)-types \( p \in S_n^F(k) \) are determined by the prime ideals of \( k[x_1, \dots, x_n] \).
    For such a type \( p \), we can define a prime ideal by
    \[ I_p = \qty{f \in k[x_1, \dots, x_n] \mid (f(x_1, \dots, x_n) = 0) \in p} \]
    These ideals are prime, and all prime ideals arise in this way.
    The map \( p \mapsto I_p \) is a continuous bijection from the type space \( S_n^F(k) \) to the prime spectrum \( \Spec k[x_1, \dots, x_n] \) with the Zariski topology.
    Also, note that \( \abs{S_n^F(k)} \leq \abs{k} + \aleph_0 \) by Hilbert's basis theorem.
\end{example}

\subsection{Isolated points}
Recall that a point \( p \) in a topological space is \emph{isolated} if \( \qty{p} \) is an open set.
If \( p \) is isolated in \( S_n^{\mathcal M}(A) \), then
\[ \qty{p} = \bigcup_I \lBrack\varphi_i\rBrack \]
so as \( \qty{p} \) is a singleton, there must be a single formula \( \varphi = \varphi_i \) such that \( \qty{p} = \lBrack\varphi\rBrack \); we say that \( \varphi \) \emph{isolates} the type.
\begin{definition}
    Let \( \mathcal T \) be an \( \mathcal L \)-theory.
    We say that a formula \( \varphi(x_1, \dots, x_n) \) \emph{isolates} the \( n \)-type \( p \) of \( \mathcal T \) if \( \mathcal T \cup \qty{\varphi} \) is satisfiable, and
    \[ \mathcal T \vDash \forall \vb x.\, (\varphi(\vb x) \to \psi(\vb x)) \]
    for all \( \psi \in p \).
\end{definition}
\begin{proposition}
    If \( \varphi \) isolates \( p \), then \( p \) is realised in any model of \( \mathcal T \cup \qty{\exists \vb x.\, \varphi(\vb x)} \).
    In particular, if \( \mathcal T \) is a complete theory, then all isolated types are realised.
\end{proposition}
\begin{proof}
    If \( \mathcal M \) is a model of \( \mathcal T \) and there exists \( \vb a \) such that \( \mathcal M \vDash \varphi(\vb a) \), then clearly \( \vb a \) realises \( p \) in \( \mathcal M \).
    If \( \mathcal T \) is complete, then either
    \[ \mathcal T \vDash \exists \vb x.\, \varphi(\vb x) \]
    or
    \[ \mathcal T \vDash \forall \vb x.\, \neg \varphi(\vb x) \]
    If \( \varphi \) isolates \( \mathcal T \), then \( \mathcal T \cup \qty{\varphi} \) is satisfiable by definition, so the latter case is impossible.
\end{proof}

\subsection{Omitting types}
\begin{theorem}[omitting types theorem]
    Let \( \mathcal L \) be a countable language and let \( \mathcal T \) be an \( \mathcal L \)-theory.
    Let \( p \) be a non-isolated \( n \)-type of \( \mathcal T \).
    Then there is a countable model \( \mathcal M \vDash \mathcal T \) that omits \( p \).
\end{theorem}
\begin{proof}
    Let \( C = \qty{c_0, c_1, \dots} \) be a countable set of new constants.
    We expand \( \mathcal T \) to a consistent \( \mathcal L_C \)-theory \( \mathcal T^\star \) by adding recursively defined sentences \( \theta_0, \theta_1, \dots \).
    We will do this in such a way that \( \theta_t \to \theta_s \) for all \( s < t \).
    To build the \( \theta \), we first enumerate the \( n \)-tuples \( C^n = \qty{\vb d_0, \vb d_1, \dots} \), and enumerate the \( \mathcal L_C \)-sentences \( \varphi_0, \varphi_1, \dots \).

    Start with \( \theta_0 = \forall x.\, x = x \), which is trivially true.
    Suppose we have already constructed \( \theta_s \) in such a way that \( \mathcal T \cup \qty{\theta_s} \) is consistent.

    First, suppose \( s = 2i \).
    These sentences will be designed to turn \( C \) into the domain of an elementary substructure of some model of \( \mathcal T^\star \).
    Suppose that \( \varphi_i = \exists x.\, \psi(x) \) is existential, with parameters in \( C \) as \( \varphi \) is an \( \mathcal L_C \)-formula.
    Suppose \( \mathcal T \vDash \theta_s \to \varphi_i \).
    As only finitely many constants from \( C \) have been used so far, we can find some unused \( c \in C \).
    Let
    \[ \theta_{s + 1} = \theta_s \wedge \psi(c) \]
    If \( \mathcal N \) models \( \mathcal T \cup \qty{\theta_s} \), then there is a witness to \( \psi \) in \( \mathcal N \), so we can interpret \( c \) as this witness.
    Thus, \( \mathcal N \) models \( \mathcal T \cup \qty{\theta_{s+1}} \), so this theory is consistent.
    If \( \varphi_i \) is not existential, or \( \mathcal T \nvDash \theta_s \to \varphi_i \), then define \( \theta_{s + 1} = \theta_s \).

    Now, suppose \( s = 2i + 1 \).
    These sentences will be designed to ensure that \( C \) omits \( p \).
    Let \( \overline d_i = (e_1, \dots, e_n) \).
    Remove every occurrence of the \( e_j \) from \( \theta_s \) by replacing it with the variable \( x_j \), and replace every occurrence of other constants in \( C \) with a fresh variable \( x_c \), together with a quantifier \( \exists x_c \) in front of the formula.
    This yields an \( \mathcal L \)-formula \( \psi(x_1, \dots, x_n) \).
    For example, if
    \[ \theta_s = \forall x.\, \exists y.\, (rx + e_1 e_2 = y^2 + t e_2);\quad r \neq t \in C \]
    then
    \[ \psi(x_1, x_2) = \exists x_r.\, \exists x_t.\, \forall x.\, \exists y.\, (x_r x + x_1 x_2 = y^2 + x_t x_2) \]
    As \( p \) is not isolated, there is no \( \mathcal L \)-formula that isolates it, so there must be some \( \varphi(\vb x) \in p \) that is not implied by \( \psi(\vb x) \); otherwise \( \psi \) would isolate the type \( p \).
    We define \( \theta_{s+1} \) in such a way that \( \vb d_i \) cannot realise \( p \).
    \[ \theta_{s + 1} = \theta_s \wedge \neg \varphi(\vb d_i) \]
    This is consistent, because there must be some \( \vb n \in \mathcal N \vDash \mathcal T \) such that
    \[ \mathcal N \vDash \psi(\vb n) \wedge \neg \psi(\vb n) \]
    and we can turn \( \mathcal N \) into an \( \mathcal L_C \)-structure that models \( \theta_{s+1} \) by interpreting \( \vb d_i \) as \( \vb n \), and interpreting the constants in \( C \) but not in \( \vb d \) as the respective witnesses to the existential statements \( \exists x_c \) within \( \psi \).

	Let \( \mathcal T^\star \) be \( \mathcal T \) together with all of the \( \theta_s \).
	Note that each \( \mathcal T \cup \qty{\theta_s} \) is consistent, and each \( \theta_{s+1} \) implies \( \theta_s \), so by compactness, \( \mathcal T^\star \) must be consistent.
	Moreover, if \( \mathcal M \) is a model of \( \mathcal T^\star \), the construction of \( \theta_{2i+1} \) ensures that \( C \) has a witness to \( \varphi_i \) that holds in \( \mathcal M \).
	Thus, by that Tarski--Vaught test, \( \mathcal C \) is the domain of an elementary substructure of \( \mathcal M \).
	If \( \vb c \in C \vDash \mathcal T^\star \), then \( \vb c = \vb d_i \) for some \( i \).
	As \( C \vDash \theta_{2i + 2} \), we have \( \neg \varphi(\vb c) \) for some \( \varphi \) in the type \( p \).
	Hence \( \vb c \) cannot realise the type \( p \) in \( C \).
\end{proof}
\begin{remark}
	The proof can be generalised to omit countably many types at the same time.
\end{remark}
